A:Type, I:MaInterface(A), i:Id.
(i  ma-interface-locs(I))
 (k:Knd. (ma-interface-domb(I;i;k))  (k  ma-interface-dom(I;i))) 

latex

Definitions

ma-interface-dom(I;i), ma-interface-domb(I;i;k), MaInterface(T), ma-interface-locs(I), Knd, x:A. B(x), Id, (x  l), P  Q, Type, b, x:A  B(x), P  Q, P & Q, P  Q, a:A fp B(a), Atom$n, s = t, a < b, left + right, t  T, IdDeq, x.A(x), x. t(x), {x:A| B(x)} , State(ds), Top, x:AB(x), f(x), type List, Void, x:A.B(x), x:A. B(x), <a, b>, hasloc(k;i), S  T, IdLnk, , fpf-domain(f), ||as||, False, A, A  B, , , l[i], A c B, KindDeq, #$n, x  dom(f),

Lemmas

iff functionality wrt iff, member-fpf-domain, fpf-dom wf, decl-state wf, top wf, nat wf, length wf nat, select wf, fpf-domain wf, fpf-trivial-subtype-top, subtype rel product, subtype rel list, subtype rel function, subtype rel set, l member wf, assert wf, hasloc wf, subtype-set-hasloc, fpf-ap wf, member-fpf-dom